package nl.cwi.arne.generator.tools;

import java.io.File;

import nl.cwi.arne.Edge;
import nl.cwi.arne.Network;
import nl.cwi.arne.NetworkActivation;
import nl.cwi.arne.generator.mcrl2.ArneMCRL2Translator;
import nl.cwi.arne.lts.LTS;
import nl.cwi.arne.lts.State;
import nl.cwi.arne.lts.Transition;
import nl.cwi.arne.lts.resource.LTSResource;
import nl.cwi.arne.lts.util.LTSSearch;
import nl.cwi.arne.mcrl2.Specification;
import nl.cwi.arne.mcrl2.toolchains.GenerateLTSToolChain;
import nl.cwi.arne.mcrl2.util.MCRL2Options;
import nl.cwi.arne.util.NetworkActivationIterator;

import org.eclipse.core.runtime.IStatus;
import org.eclipse.emf.common.util.URI;
import org.eclipse.emf.ecore.util.EcoreUtil;
import org.eclipse.equinox.app.IApplicationContext;

public class SlowFastComparisonTool extends AbstractGeneratorTool {
	
	/*
	 * (non-Javadoc)
	 * @see org.eclipse.equinox.app.IApplication#start(org.eclipse.equinox.app.IApplicationContext)
	 */
	@Override
	public Object start(IApplicationContext context) throws Exception {
		
		int generated = 0;
		int fastUpTo2 = 0;
		int slowUpTo2 = 0;
		int bisimilar = 0;
		int intermediate = 0;
		
		// Read the arguments:
		Network network = loadNetwork(context);
		
		// MCRL2 translator:
		ArneMCRL2Translator translator = new ArneMCRL2Translator();
		translator.setStartFromZeroChange(true);
		
		network.setCheckEquivalence(true);
		network.setCheckModalFormula(false);
		network.setCheckStableRegions(false);
		network.getActivations().clear();
		
		// We have a slow, a fast and a none network:
		Network fast = network;
		Network slow = (Network) EcoreUtil.copy(network);
		Network none = (Network) EcoreUtil.copy(network);
		
		// Adjust the slow network:
		for (Edge edge : slow.getEdges()) {
			if (edge.getBaseLevels().isEmpty()) {
				edge.getBaseLevels().add(edge.getEndLevel());
				edge.setEndLevel(0);
				edge.setStartLevel(0);
			}
		}
		
		// Adjust the none network:
		for (Edge edge : none.getEdges()) {
			if (edge.getBaseLevels().isEmpty()) {
				edge.getBaseLevels().add((int) edge.getSource().getLevels());
				edge.setEndLevel(0);
				edge.setStartLevel(0);
			}
		}
		
		// Iterators:
		NetworkActivationIterator slowIterator = new NetworkActivationIterator(slow);
		NetworkActivationIterator fastIterator = new NetworkActivationIterator(fast);
		NetworkActivationIterator noneIterator = new NetworkActivationIterator(fast);
		MCRL2Options options = getMCRL2Options();
		
		// Generate activations:
		while (slowIterator.hasNext()) {
			
			NetworkActivation newSlow = slowIterator.next();
			NetworkActivation newFast = fastIterator.next();
			NetworkActivation newNone = noneIterator.next();
			
			File slowLTS = generateLTS(newSlow, translator, options);
			File fastLTS = generateLTS(newFast, translator, options);
			File noneLTS = generateLTS(newNone, translator, options);
			
			// Load the LTS'
			LTSResource slowResource = new LTSResource(URI.createFileURI(slowLTS.getAbsolutePath()));
			LTSResource fastResource = new LTSResource(URI.createFileURI(fastLTS.getAbsolutePath()));
			LTSResource noneResource = new LTSResource(URI.createFileURI(noneLTS.getAbsolutePath()));
			slowResource.load(null);
			fastResource.load(null);
			noneResource.load(null);

			// Rename the 'fast' actions to 'slow':
			//for (Transition transition : fastResource.getLTS().getTransitions()) {
			//	String replacement = transition.getLabel().replaceFirst("fast", "slow");
			//	transition.setLabel(replacement);
			//}
			//fastResource.save(null);
			
			// Compare the max values of the LTS'
			int slowMax = getMaxValue(slowResource.getLTS(), "e", 0);
			int fastMax = getMaxValue(fastResource.getLTS(), "e", 0);
			int noneMax = getMaxValue(noneResource.getLTS(), "e", 0);
			
			// Compare the LTS modulo bisimulation:
			//CompareLTSToolChain compare = new CompareLTSToolChain(slowLTS, fastLTS, options);
			//IStatus status = compare.execute(monitor);
			//if (status.getSeverity()!=IStatus.OK) {
			//	throw new RuntimeException("Error comparing LTSs");
			//}
			
			// Clean up:
			slowLTS.delete();
			fastLTS.delete();
			noneLTS.delete();
			
			/*
			if (slowMax!=fastMax) {
				System.out.println("\n\n" + newSlow);
				System.out.println("SLOW: " + slowMax);
				System.out.println("FAST: " + fastMax + "\n");
				network.getActivations().add(newFast);
				if (fastMax==2) {
					fastUpTo2++;
				}
				else if (slowMax==2) {
					slowUpTo2++;
				}
			}
			
			if (compare.getResult()) {
				bisimilar++;
			}
			*/
			if (noneMax!=fastMax && fastMax!=slowMax) {
				network.getActivations().add(newFast);
				System.out.println("\nFOUND  " + newFast);
				intermediate++;
			}
			
			generated++;
			System.out.println((noneMax+"") + (fastMax+"") + (slowMax+"") + "     generated " + generated + "  found " +intermediate);
			
		}
		
		System.out.println("\n");
		System.out.println("GENERATED:    " + generated);
		System.out.println("SLOW_UP_TO_2: " + slowUpTo2 + "  (and fast not)");
		System.out.println("FAST_UP_TO_2: " + fastUpTo2 + "  (and slow not)");
		System.out.println("BISIMILAR:    " + bisimilar);
		System.out.println("INTERMEDIATE: " + intermediate);
		
		network.eResource().save(null);
		
		return null;
		
	}
	
	private File generateLTS(NetworkActivation activation, ArneMCRL2Translator translator, MCRL2Options options) {
		Specification spec = translator.generateSpecification(activation);
		GenerateLTSToolChain toolchain = new GenerateLTSToolChain(spec, options);
		IStatus status = toolchain.execute(monitor);
		if (status.getSeverity()!=IStatus.OK) {
			throw new RuntimeException("Error generating LTSs");
		}
		return toolchain.getLTSFile();
	}
	
	private int getMaxValue(LTS lts, final String name, int initial) {
		max = initial;
		new LTSSearch() {
			protected boolean shouldStop(State state, Path path) {
				// Check all outgoing transitions
				for (Transition next : state.getOutgoing()) {
					updateMax(next, name);
				}
				return false;
			}
		}.depthFirst(lts.getInitialState(), false);
		return max;
	}
	
	private void updateMax(Transition transition, String name) {
		String[] label = transition.getParsedLabel();
		if (label[1].equals(name)) {
			int level = Integer.parseInt(label[2]);
			if (level>max) max = level;
		}
	}
	
	int max;
	
	
}
